propositions as types
propositions as types(型としての命題)
証明を関数(λ項: 証明項と呼ぶ)、命題を証明項のデータ型とみなす
$ \begin{array}{c|c} \mathrm{英語} & \mathrm{型理論} \\ \hline \mathrm{True} & \mathbf{1} \\ \mathrm{False} & \mathbf{0} \\ \text{A and B} & A \times B \\ \text{A or B} & A + B \\ \text{If A then B} & A \rightarrow B \\ \text{A if and only if B} & (A \rightarrow B ) \times (B \rightarrow A) \\ \text{Not A} & A \rightarrow \mathbf{0} \end{array}
参考
メモ